\begin{tabbing} $\forall$\=${\it es}$:event\_system\{i:l\}, $i$,$a$:Id, $p$:finite{-}prob{-}space, ${\it ds}$:fpf(Id; $x$.Type),\+ \\[0ex]$P$:(decl{-}state(${\it ds}$)$\rightarrow\mathbb{B}$). pre{-}p(${\it es}$; $i$; ${\it ds}$; $a$; $p$; $P$) $\in$ prop\{i:l\} \- \end{tabbing}